Inference at * 1 
Iof proof for Lemma adjacent-member:



1. T : Type
2. L : T List
3. x : T
4. y : T
5. adjacent(T;L;x;y)
6. x before y  L
7. (y  L)
8. (x  L)
  {(x  L) & (y  L)} 

latex

 by ((Unfold `guard` ( 0)) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

{T}, x before y  l, adjacent(T;L;x;y), type List, Type, P & Q, x:A  B(x), (x  l)